\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Cmd}$, ${\it Rsp}$:Type, ${\it isupdate}$:(${\it Cmd}$$\rightarrow\mathbb{B}$), ${\it Delta}$:((\{$c$:${\it Cmd}$$\mid$ $\uparrow$(${\it isupdate}$($c$))\}  List)$\rightarrow$${\it Rsp}$),\+
\\[0ex]$Q$:((\{$c$:${\it Cmd}$$\mid$ $\uparrow$(${\it isupdate}$($c$))\}  List)$\rightarrow$\{$c$:${\it Cmd}$$\mid$ $\neg$($\uparrow$(${\it isupdate}$($c$)))\} $\rightarrow$${\it Rsp}$),
\\[0ex]${\it In}$:AbsInterface(${\it Cmd}$), ${\it Out}$:AbsInterface(${\it Rsp}$), ${\it Sys}$:AbsInterface(${\it Cmd}$ List),
\\[0ex]$f$:sys{-}antecedent(${\it es}$;${\it Sys}$).
\-\\[0ex]abstract{-}chain{-}replication\{i:l\}(${\it es}$; ${\it Cmd}$; ${\it Rsp}$; ${\it isupdate}$; ${\it In}$; ${\it Out}$; ${\it Sys}$; $f$; ${\it Delta}$; $Q$) $\in$ $\mathbb{P}$
\end{tabbing}